Consider the TRS R consisting of the rewrite rules
1:
D(t)
→ 1
2:
D(constant)
→ 0
3:
D(x + y)
→ D(x) + D(y)
4:
D(x * y)
→ (y * D(x)) + (x * D(y))
5:
D(x - y)
→ D(x) - D(y)
There are 6 dependency pairs:
6:
D#(x + y)
→ D#(x)
7:
D#(x + y)
→ D#(y)
8:
D#(x * y)
→ D#(x)
9:
D#(x * y)
→ D#(y)
10:
D#(x - y)
→ D#(x)
11:
D#(x - y)
→ D#(y)
The approximated dependency graph contains one SCC:
{6-11}.
Consider the SCC {6-11}.
There are no usable rules.
By taking the AF π with
π(D#) = 1 together with
the lexicographic path order with
empty precedence,
the rules in {6-11}
are strictly decreasing.